es:ES{i}, e:E, ds:x:Id fp Type{i}, P:(State(ds)Prop{i'}), j:Id. e:s.P(s)@j   Prop{i'} 

latex

Definitions	ES, t  T, x:A. B(x), E, Id, Type, x.A(x), x. t(x), Prop, State(ds), x:AB(x), loc(e), s = t, {x:A| B(x) }, (e < e'), (e <loc e'), x:AB(x), P & Q, x:A. B(x), Top, IdDeq, f(x)?z, vartype(i;x), P  Q, state@i, (state when e), f(a), left+right, x(s), P  Q, e@i. P(e), state after e, A & B, a:A fp B(a), e:s.P(s)@j
Lemmas	es-state-after wf, alle-at wf, event system-level-subtype, es-state-when wf, subtype rel dep function, subtype rel self, es-vartype wf, fpf-cap wf, id-deq wf, top wf, es-locl wf, es-causl wf, es-loc wf, decl-state wf, fpf wf, Id wf, es-E wf, event system wf